#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include <cctype>
#include <list>
#include "skip_list2.h"

#ifdef __linux__
#include "x86intrin.h"
#else
#include <inttypes.h>
#include <intrin.h>
#endif

namespace solver 
{

	const uint64_t big_int_native_bits = 64;
	const uint64_t big_int_max_ints = 200;
	const uint64_t big_int_max_bits = big_int_max_ints * 64;

	class big_int_convert 
	{
	public:

		static uint64_t bit_to_index(uint64_t bit)
		{
			uint64_t t = (bit / big_int_native_bits);
			return big_int_max_ints - (t+1);
		}

		static uint64_t index_to_bit(uint64_t index)
		{
			uint64_t idx = (big_int_max_ints - (index + 1));
			return idx * big_int_native_bits;
		}

		static uint64_t bit_to_indexed_bit(uint64_t bit)
		{
			return bit % big_int_native_bits;
		}

		static std::string run_count_char(char*& p, char match)
		{
			std::string temp = "";
			int runcount = 0;
			while (*p && *p == match)
			{
				p++;
				runcount++;
			}
			switch (runcount)
			{
			case 0:
				break;
			case 1:
			case 2:
			case 3:
			case 4:
				temp.append(runcount, match);
				break;
			default:
				temp += "[";
				temp += std::to_string(runcount);
				temp += ":";
				temp += match;
				temp += "]";
				break;
			}
			return temp;
		}

		static std::string pack_bit_string(char *p)
		{
			std::string temp = "";
			while (*p && *p == '0')
				p++;
			int runcount = 0;
			while (*p) {
				temp += run_count_char(p, *p);
			}
			return temp;
		}


	};

	class packed_big_int_item
	{
	public:

		int		 index;
		uint64_t mask;
		uint64_t value;

		packed_big_int_item() : index(0), mask(0), value(0)
		{

		}
	};

	class packed_big_int
	{
	public:

		skip_lists::skip_list_type<int, packed_big_int_item, skip_lists::int_compare_type> items;
		typedef skip_lists::skip_list_type<int, packed_big_int_item, skip_lists::int_compare_type>::node_type item_node;

		packed_big_int() : items(0, packed_big_int_item())
		{
			;
		}

		packed_big_int(const packed_big_int& src) : items(src.items)
		{
			;
		}

		packed_big_int(packed_big_int&& src) : items(0, packed_big_int_item() )
		{
			items = std::move( src.items );
		}

		void operator = (packed_big_int& src)
		{
			items = src.items;
		}

		void operator = (packed_big_int&& src)
		{
			items = std::move( src.items );
		}

		bool set_bit(uint64_t bit_index, uint64_t value)
		{
			if (bit_index >= big_int_max_bits)
				return false;

			uint64_t global_index = big_int_convert::bit_to_index(bit_index);
			uint64_t local_index = big_int_convert::bit_to_indexed_bit(bit_index);
			item_node *f = nullptr;
			
			f = items.find(global_index);
			if (f == nullptr) 
			{
				packed_big_int_item bi;
				bi.index = global_index;
				bi.mask |= (1LL << local_index);
				bi.value |= (value << local_index);
				items.update(global_index, bi);
			}
			else 
			{
				auto bi = &f->value;
				bi->mask |= (1LL << local_index);
				bi->value |= (value << local_index);
			}

			return true;
		}

		std::string to_string()
		{
			std::string temp = "";

			int l = (items.size()+8)*big_int_native_bits;

			char *tempBuff = new char[l + 1];
			tempBuff[l] = 0;
			int bk = 0;
			auto idx = items.first();
			while (idx != nullptr)
			{
				bk += sprintf(&tempBuff[bk], "@%ld-", idx->value.index);
				auto bts = idx->value.value;
				for (int64_t k = big_int_native_bits - 1; k >= 0; k--)
				{
					uint64_t bt = 1LL << k;
					if ((bts & bt) == bt) {
						tempBuff[bk] = '1';
					}
					else {
						tempBuff[bk] = '0';
					}
					bk++;
				}
				idx = items.next(idx);
			}
			temp = big_int_convert::pack_bit_string(tempBuff);
			delete[] tempBuff;

			return temp;
		}


	};

	class big_int 
	{
		uint64_t *bits;
		bool overflow;

	public:

		bool get_overflow() { return overflow;  }

		big_int() : overflow(false)
		{
			bits = new uint64_t[big_int_max_ints];
			for (int i = 0; i < big_int_max_ints; i++)
			{
				bits[i] = 0;
			}
		}

		virtual ~big_int()
		{
			if (bits)
				delete[] bits;
			bits = nullptr;
		}

		void operator = (const big_int& src)
		{
			big_int t;
			for (int i = 0; i < big_int_max_ints; i++)
			{
				bits[i] = src.bits[i];
			}
			overflow = src.overflow;
		}

		big_int(const big_int& src) :big_int()
		{
			*this = src;
		}

		big_int(big_int&& src)
		{
			bits = src.bits;
			overflow = src.overflow;
			src.bits = nullptr;
		}

		void operator = (big_int&& src)
		{
			bits = src.bits;
			overflow = src.overflow;
			src.bits = nullptr;
		}

		bool add(uint64_t bit_index)
		{

			if (bit_index >= big_int_max_bits) 
			{
				overflow = true;
				return false;
			}

			bool carry = true;

			// really need to do some assembly for this sort of thing but there is no time! 
			while (carry)
			{
				int global_index = big_int_convert::bit_to_index(bit_index);
				int local_index = big_int_convert::bit_to_indexed_bit(bit_index);
				uint64_t local = 1LL << local_index;
				uint64_t bito = bits[global_index];

				carry = ::_addcarry_u64(false, local, bito, &bits[global_index]);
				if (carry) 
				{
					global_index--;
					if (global_index < 0)
						return false;
					bit_index = big_int_convert::index_to_bit( global_index );
				}
			}

			return true;
		}

		bool test(packed_big_int* comparison)
		{
			bool success = true;
			for (auto ix = comparison->items.first(); success && ix != nullptr; ix = comparison->items.next(ix)) 
			{
				uint64_t bv = bits[ix->value.index];
				uint64_t temp = bv & ix->value.mask;
				success = temp == ix->value.value;
			}
			return success;
		}

		std::string to_string()
		{
			std::string temp = "";

			if (overflow)
			{
				temp = "OVF";
			}

			int first_idx = 0;
			int l = 0;
			while (first_idx < big_int_max_ints && bits[first_idx] == 0) {
				first_idx++;
			}
			l = (big_int_max_ints - first_idx) * big_int_native_bits;

			if (first_idx == big_int_max_ints)
			{
				temp += "0";
			}
			else 
			{
				char *tempBuff = new char[l + 1];
				tempBuff[l] = 0;
				int bk = 0;
				int idx = first_idx;
				while (idx <  big_int_max_ints)
				{
					auto bts = bits[idx];
					for (int64_t k = big_int_native_bits - 1; k >= 0; k--)
					{
						uint64_t bt = 1LL << k;
						if ((bts & bt) == bt) {
							tempBuff[bk] = '1';
						}
						else {
							tempBuff[bk] = '0';
						}
						bk++;
					}
					idx++;
				}
				temp = big_int_convert::pack_bit_string(tempBuff);
				delete[] tempBuff;
			}
			return temp;
		}

		void clear()
		{
			overflow = false;
			for (int i = 0; i < big_int_max_ints; i++)
			{
				bits[i] = 0;
			}
		}

		void set_bit(uint64_t bit_index, uint64_t value)
		{
			uint64_t global_index = big_int_convert::bit_to_index(bit_index);
			uint64_t local_index = big_int_convert::bit_to_indexed_bit(bit_index);
			uint64_t local_value = value << local_index;
			uint64_t local_mask = 1LL << local_index;
			bits[global_index] &= ~local_mask;
			bits[global_index] |= local_value;
		}

		uint64_t get_bit(uint64_t bit_index)
		{
			uint64_t global_index = big_int_convert::bit_to_index(bit_index);
			uint64_t local_index = big_int_convert::bit_to_indexed_bit(bit_index);
			uint64_t local_mask = 1LL << local_index;
			uint64_t ret = (bits[global_index] & local_mask) >> local_index;
			return ret;
		}

		static void self_test(std::list<std::string>& results)
		{
			big_int a;
			big_int b;
			big_int x;
			std::string temp;

			x.set_bit(0, 1);
			temp = x.to_string();
			if (temp.compare("1") != 0)
			{
				temp = "bigint x0 got " + temp;
				results.push_back(temp);
			}

			x.set_bit(10, 1);
			temp = x.to_string();
			if (temp.compare("1[9:0]1") != 0)
			{
				temp = "bigint x1 got " + temp;
				results.push_back(temp);
			}

			x.set_bit(0, 0);
			temp = x.to_string();
			if (temp.compare("1[10:0]") != 0)
			{
				temp = "bigint x2 got " + temp;
				results.push_back(temp);
			}

			x.set_bit(74, 1);
			temp = x.to_string();
			if (temp.compare("1[63:0]1[10:0]") != 0)
			{
				temp = "bigint x1 got " + temp;
				results.push_back(temp);
			}

			x.set_bit(10, 0);
			temp = x.to_string();
			if (temp.compare("1[74:0]") != 0)
			{
				temp = "bigint x2 got " + temp;
				results.push_back(temp);
			}

			for (int i = 0; i < 5; i++)
			{
				a.add(i);
			}
			temp = a.to_string();
			if (temp.compare("[5:1]") != 0)
			{
				temp = "bigint 0 got " + temp;
				results.push_back(temp);
			}

			b.add(0);
			temp = b.to_string();
			if (temp.compare("1") != 0) {
				temp = "bigint a got " + temp;
				results.push_back(temp);
			}
			b.add(0);
			temp = b.to_string();
			if (temp.compare("10") != 0) {
				temp = "bigint b got " + temp;
				results.push_back(temp);
			}
			b.add(0);
			temp = b.to_string();
			if (temp.compare("11") != 0) {
				temp = "bigint c got " + temp;
				results.push_back(temp);
			}
			b.add(63);
			temp = b.to_string();
			if (temp.compare("1[61:0]11") != 0) {
				temp = "bigint d got " + temp;
				results.push_back(temp);
			}
			b.add(127);
			temp = b.to_string();
			if (temp.compare("1[63:0]1[61:0]11") != 0) {
				temp = "bigint e got " + temp;
				results.push_back(temp);
			}
			b.add(4);
			temp = b.to_string();
			if (temp.compare("1[63:0]1[58:0]10011") != 0) {
				temp = "bigint f got " + temp;
				results.push_back(temp);
			}
			b.add(127);
			temp = b.to_string();
			if (temp.compare("1[64:0]1[58:0]10011") != 0) {
				temp = "bigint g got " + temp;
				results.push_back(temp);
			}
			b.add(0);
			temp = b.to_string();
			if (temp.compare("1[64:0]1[58:0]10100") != 0) {
				temp = "bigint h got " + temp;
				results.push_back(temp);
			}

			packed_big_int pb;

			pb.set_bit(2, 1);
			pb.set_bit(1, 0);
			pb.set_bit(0, 0);

			temp = pb.to_string();

			if (!b.test(&pb)) 
			{
				temp = "bigint k test failed";
				results.push_back(temp);
			}

			big_int c;
			for (int i = big_int_max_bits - 8; i >= 0; i--)
			{
				c.add(i);
			}

			temp = c.to_string();
			if (temp.compare("[12793:1]") != 0) {
				temp = "bigint i got " + temp;
				results.push_back(temp);
			}

			packed_big_int pb2;

			pb2.set_bit(12792, 1);
			pb2.set_bit(512, 1);
			pb2.set_bit(256, 1);
			pb2.set_bit(128, 1);
			pb2.set_bit(2, 1);
			pb2.set_bit(1, 1);
			pb2.set_bit(0, 1);

			if (!c.test(&pb2))
			{
				temp = "bigint k2 test failed";
				results.push_back(temp);
			}

			c.add(0);
			temp = c.to_string();
			if (temp.compare("1[12793:0]") != 0) {
				temp = "bigint j got " + temp;
				results.push_back(temp);
			}

			if (c.test(&pb2))
			{
				temp = "bigint k3 test failed";
				results.push_back(temp);
			}

			packed_big_int pb3;

			pb3.set_bit(12793, 1);
			pb3.set_bit(512, 0);
			pb3.set_bit(256, 0);
			pb3.set_bit(128, 0);
			pb3.set_bit(2, 0);
			pb3.set_bit(1, 0);
			pb3.set_bit(0, 0);

			if (!c.test(&pb3))
			{
				temp = "bigint k4 test failed";
				results.push_back(temp);
			}

		}
	};
}
